Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add script to run CI locally #23

Merged
merged 3 commits into from
Jan 13, 2024
Merged

Add script to run CI locally #23

merged 3 commits into from
Jan 13, 2024

Conversation

jlapeyre
Copy link
Collaborator

  • This is the same CI that runs remotely automatically with PRs. This is a posix shell script.
  • Remove a bit of cruft as well

* This is the same CI that runs remotely automatically with PRs. This is a
  posix shell script.
* Remove a bit of cruft as well
local_CI.sh Outdated
@@ -0,0 +1,6 @@
#!/bin/env sh
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

btw, this hashbang makes all the scripts invalid for execution on quite a lot of systems - Mac for example puts env in /usr/bin with no symlink of it from /bin.

Personally I actually thought env typically lived in /usr/bin on most systems, but I guess not if it's in /bin on yours.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh yeah. I have bin ⇒ usr/bin

.gitignore Outdated
@@ -15,3 +15,4 @@ crates/oq3_syntax/src/ast/generated/_new_tokens.rs
.env/
.envs/
.ackrc
save/
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What generates this?

(a bunch of the files in here look like particular files from your directory - you might want to move those to your user-local .git/info/exclude rather than having the ignores commited for everyone)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes that's either cruft or particular things that can be move.

@jlapeyre
Copy link
Collaborator Author

jlapeyre commented Jan 12, 2024

Thanks for reviewing. I think the latest commits take care of these problems.

@jlapeyre jlapeyre merged commit 15d9220 into main Jan 13, 2024
2 checks passed
@jlapeyre jlapeyre deleted the local-ci-script branch January 23, 2024 16:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants